\begin{tabbing}
$\forall$\=$k$:Knd, $T$:Type, $l$:IdLnk, ${\it ds}$, ${\it dt}$:${\it tg}$:Id fp$\rightarrow$ Type,\+
\\[0ex]$g$:(${\it tg}$:Id$\times$(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$(DeclaredType(${\it dt}$;${\it tg}$) List))) List.
\-\\[0ex](\=isrcv($k$)\+
\\[0ex]$\Rightarrow$ destination(lnk($k$)) $=$ source($l$) $\in$ Id \& (lnk($k$) = $l$ $\Rightarrow$ $T$ $=$ DeclaredType(${\it dt}$;tag($k$))))
\-\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it dt}$)
\\[0ex]$\Rightarrow$ \=sends $k$(v:$T$) on $l$:\+
\\[0ex]tagged($g$,State(${\it ds}$),v):${\it dt}$
\\[0ex]$\Vdash$ ${\it es}$.\=sends $k$(v:$T$) on $l$:\+
\\[0ex]tagged($g$,State(${\it ds}$),v):${\it dt}$
\-\-
\end{tabbing}